a, b, c:. a + c  b  b + c  a  0 < c  False 

latex

Definitions

P & Q, x. t(x), , True, T, P  Q, P  Q, {T}, SQType(T), q-rel(r;x), xL. P(x), A c B, t.2, (i = j), tl(l), ff, b, i z j, nth_tl(n;as), hd(l), l[i], tt, ||as||, i <z j, t.1, if b then t else f fi , Y, A, A  B, , , as[i]?a, q-constraints(k;A;y), x:A. B(x), False, t  T, P  Q, x:A. B(x), x(s), (x  l), decidable q-rel, decidable l all-better-extract, q-rel-lub(r1;r2), map(f;as), upto(n), normalize-constraint(k;p), as @ bs, map-eval(x.f(x);L), normalize-constraints(k;A), r * s, r - s, qpositive(r), p q, q_le(r;s), <+>, , gset, goset, , x f y, p  q, a < b, q_less(a;b), reduce(f;k;as), filter(P;l), product-map, exists functionality wrt iff, decidable int equal, decidable false, qeq(r;s), decidable equal rationals, decidable implies, decidable not, decidable and, list_accum(x,a.f(x;a);y;l), decidable l exists better-extract, decidable q-constraints-opt, P  Q, Dec(P), r + s, S  T

Lemmas

qmul zero qrng, qadd inv assoc q, qinverse q, qadd comm q, qadd ac 1 q, mon assoc q, qmul one qrng, mon ident q, qadd preserves qless, qadd preserves qle, l member wf, pi1 wf, q-linear wf, pi2 wf, q-rel wf, q-linear-base, qmul wf, q-linear-unroll, true wf, squash wf, decidable int equal, not wf, select? wf, le wf, q-constraints wf, decidable wf, nat wf, rationals wf, qadd wf, qle wf, int inc rationals, qless wf